p-inject(A;B;f)
== x, y:A.
== (can-apply(f;x))  (can-apply(f;y))  (do-apply(f;x) = do-apply(f;y))  (x = y) 

latex

---

clarification:

p-inject(A;B;f)
== x:A, y:A.
== (can-apply(f;x))
==  (can-apply(f;y))
==  (do-apply(f;x) = do-apply(f;y)  B)
==  (x = y  A) 

latex

Definitions	x:A. B(x), b, can-apply(f;x), P  Q, do-apply(f;x), s = t
FDL editor aliases	p-inject